the_es:ES, e':E, l:IdLnk, n:(||sends(l;e')||+1), m:Msg.
(m  snds(l, before(e',n)))

(e:E. (e <loc e') & (m  sends(l;e)))  (i:n. m = sends(l;e')[i]) 

latex

Definitions	ES, IdLnk, snds(l, before(e,n)), as @ bs, snds(l;before(e)), firstn(n;as), P  Q, P  Q, P  Q, E, (e <loc e'), (x  l), x:A. B(x), Prop, l[i], sends(l;e), S  T, x:A. B(x), {i..j}, i  j < k, AB, P & Q, A, False, P  Q, Msg, ||as||, (Msg on l), t  T
Lemmas	es-sends wf, select wf, l member wf, firstn wf, es-snds wf, es-locl wf, int seg wf, append wf, member-firstn, or functionality wrt iff, iff functionality wrt iff, member-es-snds, member append, es-Msg wf, es-Msgl wf, length wf1, IdLnk wf, es-E wf, event system wf